package com.Clause.Biais;

import java.util.ArrayList;

import com.Clause.Clause;
import com.Clause.ClauseProxy;
import com.Clause.OperateurBinaire;

public class ClauseDeHorn {

	public static boolean check = false;

	public static Clause[] transformer(Clause clause){ //1 seul literal positif
		Biais.enleverParentheses(clause);  //on aura plus de parenthese, et plus dde negatif devant
		ArrayList<ClauseProxy> tetes = new ArrayList<ClauseProxy>();
		clauseDeHorn(clause.getRoot().getSuivant(),tetes);
		
		Clause[] clauses  = new Clause[tetes.size()];
		for(int i=0;i<clauses.length;++i){
			clauses[i] = copieGauche(clause);
			clauses[i].getRoot().getElement().setSuivant(tetes.get(i));
		}
		return clauses;
	}
	
	private static Clause copieGauche(Clause clause){
		Clause c2 = new Clause();
		if(clause.getRoot().getElement().getClass().equals(OperateurBinaire.class)){
			OperateurBinaire opbin = (OperateurBinaire) clause.getRoot().getElement();
			OperateurBinaire opbin2 = new OperateurBinaire(opbin);
			opbin2.setPrecedent(opbin.getPrecedent());
			c2.setRoot(opbin2);
		}
		return c2;
	}

	private static void clauseDeHorn(ClauseProxy proxy, ArrayList<ClauseProxy> tetes) { //commence avec root.suivant
		if(proxy.getElement().getClass().equals(OperateurBinaire.class)){ //operateur binaire
			OperateurBinaire opbin = (OperateurBinaire) proxy.getElement();
			if(opbin.getOperateur().equals(OperateurBinaire.ET)){
				
				
				if(opbin.getElementPrecedent().getClass().equals(OperateurBinaire.class)){
					clauseDeHorn(opbin.getPrecedent(),tetes);
				}
				else
					tetes.add(opbin.getPrecedent());
				
				if(opbin.getElementSuivant().getClass().equals(OperateurBinaire.class)){
					clauseDeHorn(opbin.getSuivant(),tetes);
				}
				else
					tetes.add(opbin.getSuivant());
			
			
			}
			else if(opbin.getOperateur().equals(OperateurBinaire.OU)){
				return;	//enlever la branche
			}
		}
	}
	
}
